COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "memo.pub[let,jmc]" source
C00016 00003	.skip 1
C00017 ENDMK
C⊗;
.require "memo.pub[let,jmc]" source;
.AT "qt" ⊂"%At%*"⊃
.AT "qw" ⊂"%Aw%*"⊃
.AT "qi" ⊂"%5 -1%*"⊃
.AT "qm" ⊂"%Am%*"⊃
.every heading (,draft,{page})
.cb EXOTIC CONTINUOUS FUNCTIONALS


.bb "1. Some examples of exotic continuous functionals."

	The fixed point theory of recursive functions is based on
continuous functionals such as qt defined by

!!a1:	%2qt[f](x) = qif p x qthen g x qelse m(x,f h x)%1.

	The theory tells us that each continuous monotonic functional
has a fixed point, and we study the fixed points of those functionals
involved in recursive definitions.  In the case of recursive definitions
%2qt[f](x)%1 is a form in which ⊗f appears as a function symbol.
However, these are not all the
continuous functions there are, and it may be interesting to study
some other examples.  Consider functionals of the form

!!a2:	%2qt[f](x) = qif p x qthen g x qelse m fqi h x%1;

that's right, we mean the inverse of the function %2f%1.  In order
to make the functional well defined and continuous, we make the
following stipulations:  First, the variable ⊗x ranges over non-negative
integers and ⊗f is a partial function from integers to integers.
Second, we define %2fqi%1 by

!!a3:	%2fqi(y) = qm x.(f(x) = y)%1,

where

!!a6:	%2qm x.p(x) ← least(0,p)%1,

and %2least(y,p)%1 is recursively defined by

!!a7:	%2least(y,p) ← qif p(y) qthen y qelse least(y+1,p)%1.

Note that the recursive definition insures that %2fqi%1 is continuous
in ⊗f, and that qmx.%2p(x)%1 is undefined if there is a value of
⊗x for which ⊗p(x) is undefined lower than a value for which ⊗p(x) 
is true.  Without this property, %2least(x,p)%1 wouldn't be monotonic
in %2p%1, and there mightn't be a least fixed point.

	Consider specializing ({eq a2}) to

!!a4:	%2qt1[f](x) = qif x = 0 qthen 0 qelse 2 + fqi(x - 1)%1.

The fixed point ⊗f1 of qt1 may be computed by iterating qt1 on %AW%1,
getting

!!a5:	%2f1 x = qif x = 0 qthen 0 qelse qif x = 1 qthen 2 qelse qif
x = 3 qthen 3 qelse qw%1,

which seems exotic if not pathological.

	Wolf Polak points out that while qt1 is exotic, its fixed point
is an ordinary recursive function, since the recursive computation
of %2fqi%1 can be spelled out.  Thus

!!a8:	%2f1 x ← qif x = 0 qthen 0 qelse 2 + f2(0,x-1)%1,

where

!!a9:	%2f2(y,x) ← qif f1(x) = y qthen x qelse f2(y+1,x)%1.

	Here is another weird functional:

!!a10:	%2qt2[f](x) = qif p x qthen g x qelse qif
f h1 x = qw ∧ f h2 x = qw qthen qw qelse f h3 x%1,

where ⊗p, ⊗g, ⊗h1, ⊗h2 and ⊗h3 are all assumed total.  (Equality here is
taken in the strong sense in which its value is always %3true%1 or %3false%1
and is never undefined).
Computing %2qt2[f](x)%1
involves a parallel computation of %2f h1 x%1 and %2f h2 x%1;
if either succeeds, the other can be stopped.  It is easily seen that the
functional is continuous and hence has a fixed point - call it ⊗f2. 
If we can use LISP functions, we can write an ordinary recursive
definition of ⊗f2, namely

!!a11:	%2f2 x ← qif p x qthen g x qelse (λy. f2 h3 x)(f2'(list(x),qNIL))%1,

with

!!a12:	%2f2'(u,v) ← qif qn u qthen (qn v ∨ f2(v,qnil))
qelse p h1 qa u ∨ p h2 qa u ∨ f2'(qd u, h1 qa u . (h2 qa u . v))%1.

[Carolyn Talcott points out that the above redefinition is not
correct and has an alternate breadth first search, but hadn't proved
hers correct to her satisfaction at last discussion].

If we are not allowed to use LISP functions, then ⊗f2 may be one of
Hewitt's and Paterson's (197x) examples of functions that can be written
with parallel programs but not with recursive programs.


.bb "2. When is a functional definable by a term?"

	In view of the above examples, we can try to characterize
those continuous functional for which %2qt[f](x)%1 can be written
as a term in ⊗f and ⊗x in which ⊗f appears as a function symbol and
⊗x as an individual variable.  Let's call them %2term functionals%1.

	If qt is a continuous functional, then the value of
%2qt[f](x)%1 depends on the value of ⊗f(y) for only a finite
number of %2y%1's.  Namely, there exist %2y%41%2,_..._,y%4k%1
such that ⊗f(y) can be changed for any ⊗y different from the %2y%4i%1's
without changing the value of %2qt[f](x)%1.  In general ⊗k depends
on the particular ⊗f and ⊗x, but when qt is a term functional, ⊗k is
bounded by the number of occurrences of ⊗f in the term %2qt[f](x)%1.
In our first exotic example, the number of ⊗f(y) on which %2qt[f](x)%1
depends is unbounded, because, depending on ⊗f, any finite number of
of %2f(x)%1's may have to be examined to compute %2fqi(y)%1.
Tentatively, we shall call a functional where such a bound exists
%2uniformly continuous%1, although we have not yet been able to
establish any properties in common with the corresponding property
in analysis.  Thus all %2term functionals%1 are %2uniformly continuous%1.

	The second exotic functional is uniformly continuous but still
isn't a term functional.  Indeed every term functional has the another
property that we may call %2sequentiality%1:

	Suppose that in evaluating %2qt[f](x)%1, we have already evaluated
%2f(x1),f(x2),_...,f(xk)%1.  There are two possibilities;  Either the
value of %2qt[f](x)%1 is already determined by these values or ⊗f(y) must
be computed for additional %2y%1's.  We call qt %2sequential%1 if
in the latter case there is always at least one ⊗y such that %2qt[f](x)%1_=_qw%1
unless %2f(y)_≠_qw%1.  The function qt2 of the previous section is not
sequential.  If qt is sequential we can always write

!!b6:	%2qt[f](x) = qif p1 x qthen g1 x qelse α{f h1 xα}[λx1.qif p2(x,x1)
qthen g2(x,x1) qelse α{f h2(x,x1)α}[λx2.qif p3(x,x1,x2) qthen g3(x,x1,x2)
qelse α{f h3(x,x1,x2α}[λx3.qif ... etc. ]]]%1.

[We use the notation %2α{argα}fn%1 for %2fn(arg)%1 when it is more convenient
to write the argument before the function].

[Note of Feb 9, 1979: The above is not quite right, because qt may evaluate
⊗f applied to various constants before asking for any of the actual arguments
⊗x, ⊗y, etc.].

	We can avoid the lengthening formulas of ({eq b6}) by writing

!!b6a:	%2qt[f](x0) = qif p1 x0 qthen g1 x0 qelse α{m1(x0,f h1 x0)α}[λx1.qif p2 x1
qthen g2 x1 qelse α{m2(x1,f h2 x1)α}[λx2.qif p3 x2 qthen %1etc.

	Given that qt is sequential, there are two possibilities.  If
qt is also %2uniformly continuous%1 the sequence of terms given in ({eq b6})
will be finite - otherwise not.  If the %2p%1's, %2g%1's and %2h%1's
are all computable in some collection %2C%1 of base functions, then we will
call qt computable if it is sequential and bounded.  In that case its
least fixed point will also be a computable function in %2C%1.

	While sequentiality
requires that some %2f(x)%1 be required for the definedness of %2qt[f](x)%1,
it doesn't require that %2h(x)%1 be unique.  Thus if

!!b7:	%2qt[f](x) = f(m x) + f(n x)%1,

we can take either %2h1_x_=_m_x%1 or %2h1_x_=_n_x%1.


.bb "3. Additional remarks."

	1. Here are some more continuous %2qt[f](x)%1:

a. %2f(x) ≠ qw%1 for at least one ⊗x. 

b. %2f(x)+x ε A%1 for at least 20 odd values of ⊗x. 

c. %2R1(x,f h1 x) ∧ R2(x,f f h2 x)%1 for at least 20 ⊗x. 

d. The functional

	%2qt[f](x) = qif p1 x qthen g x qelse qif ∃z.(f h1 z ≠ qw) qthen
f h2 z qelse qw%1

is continuous.  It can't be computed for general ⊗f except by
parallel evaluator, but its fixed point can apparently be sequentially
computed provided the domain of ⊗x can be effectively enumerated.

	2.  Note that ⊗a thru ⊗c above are predicates, and the
essential part of ⊗d is also a predicate.
Predicates play a special role, because
it is easier to define exotic continuous predicates than other functions.
The space whose elements
are just T and qw seems to play a special role.

	3. This paper is related to the problem of intensional properties
of recursive programs through the idea that intensional properties of
one program are extensional properties of "derived programs".  It is
important to ask which properties of a program are extensional properties
of the functional.  It appears that the property of being iterative is
an extensional property of the functional.

Also maximum required depth of recursion.  The test as to whether a
a finite approximation a-list is ok is f-extensional.  A function generating
a finite approximation that evaluates ⊗x is not.  What is the next
level up from the functional?  f(x)+f(x) and 2f(x) give the same functional
but different computation sequence cbn or cbv.  If we change a recursive
program by putting in a test that is never true, then we don't change the
computation sequence.  The number of occurrences of the atom CAR in the
program is changed.

Perhaps can be put into "sequential form" or changed to "sequential form",
and then certain properties will become sequential.

.<<See jan 1979 message from BCM>>
.skip 1
.begin verbatim
John McCarthy
Artificial Intelligence Laboratory
Computer Science Department
Stanford University
Stanford, California 94305

ARPANET: MCCARTHY@SU-AI
.end

.turn on "{"
%7This draft of
EXOTIC[W77,JMC]
PUBbed at {time} on {date}.%1